module Zeno.ProofLogic where

import Prelude ()
import StdImports
import Zeno.Clause

data Proof a
  = Proven !a ![Proof a]
  | Disproven !a ![Proof a]
  | Unknown
  deriving ( Eq, Ord )
  
data ProofStep a = ProofStep !String !(Clause a)
  deriving ( Eq, Ord )
  
instance Functor Proof where
  fmap f (Proven a ps) = Proven (f a) (map (fmap f) ps)
  fmap f (Disproven a ps) = Disproven (f a) (map (fmap f) ps)
  fmap _ Unknown = Unknown
  
instance Foldable Proof where
  foldMap f (Proven a ps) = f a `mappend` foldMap (foldMap f) ps
  foldMap f (Disproven a ps) = f a `mappend` foldMap (foldMap f) ps
  foldMap _ Unknown = mempty
  
instance Traversable Proof where
  sequenceA (Proven a ps) = 
    Proven <$> a <*> sequenceA (map sequenceA ps)
  sequenceA (Disproven a ps) = 
    Disproven <$> a <*> sequenceA (map sequenceA ps)
  sequenceA Unknown = 
    pure Unknown
    
instance Functor ProofStep where
  fmap f (ProofStep name cls) = ProofStep name (f <$> cls)
    
instance Foldable ProofStep where
  foldMap f (ProofStep name cls) = foldMap f cls
  
instance Traversable ProofStep where
  sequenceA (ProofStep name cls) = ProofStep name <$> sequenceA cls
  
joinStep :: a -> [Proof a] -> Proof a
joinStep a = foldr join' Unknown 
  where join' p@(Proven {}) _ = Proven a [p]
        join' p@(Disproven {}) _ = Disproven a [p]
        join' Unknown p = p
        
join :: [Proof a] -> Proof a
join = foldr join' Unknown
  where join' p@(Proven {}) _ = p
        join' p@(Disproven {}) _ = p
        join' Unknown p = p
        
addStep :: a -> Proof a -> Proof a
addStep _ Unknown = Unknown
addStep step ps@(Proven {}) = Proven step [ps]
addStep step ps@(Disproven {}) = Disproven step [ps]
        
strongJoinStep :: a -> [Proof a] -> Proof a
strongJoinStep a ps = 
  if all proven ps
    then Proven a ps
  else if all disproven ps
    then Disproven a ps
  else Unknown

anyProven :: [Proof a] -> Proof a
anyProven ps = 
  case find proven ps of
    Just p -> p
    Nothing -> Unknown
  
proven :: Proof a -> Bool
proven (Proven {}) = True
proven _ = False

disproven :: Proof a -> Bool
disproven (Disproven {}) = True
disproven _ = False
        
conjoinStep :: a -> [Proof a] -> Proof a
conjoinStep a ps = 
  case find disproven ps of
    Just disproof -> Disproven a [disproof]
    Nothing -> 
      if all proven ps
        then Proven a ps
        else Unknown
        
allProvenStep :: a -> [Proof a] -> Proof a
allProvenStep a ps = 
  if all proven ps
    then Proven a ps
    else Unknown

instance Show a => Show (Proof a) where
  show (Proven a ps) = show a ++ showProofs' ps
  show Unknown = "Unknown"
  
instance Show a => Show (ProofStep a) where
  show (ProofStep name cls) = 
    "[" ++ name ++ "] " ++ show cls

indentedBars :: Indented String
indentedBars = do
  bs <- ask
  return $ '\n' : (replicate bs ' ') ++ (replicate bs '>') 
    ++ (if bs > 0 then " " else "")
  
showProofs' :: Show a => [Proof a] -> String
showProofs' = flip runReader 0 . showProofs
    
showProofs :: Show a => [Proof a] -> Indented String
showProofs [] = do
  i <- indentedBars
  return $ i ++ "True"
showProofs [p] = showProof p
showProofs proofs@(_ : _) = indent $ do
  proofs' <- mapM showProof proofs
  {-
  i <- indentation
  let longest_lines = map (maximum . map length . lines) $ proofs'
      longest_lines' = map (\x -> x - (2 * indent)) longest_lines
      top_spacers = map (flip replicate '\\') longest_lines'
      bot_spacers = map (flip replicate '/') longest_lines'
      spacers = top_spacers `zip` bot_spacers
      proofs'' = zipWith
        (\(ts, bs) p -> i ++ ts ++ p ++ i ++ bs) spacers proofs'
  -}
  return $ "\n" ++ intercalate "\n" proofs'

showProof :: Show a => Proof a -> Indented String
showProof (Proven a ps) = do
  ps' <- showProofs ps
  i <- indentedBars
  bars <- ask
  return $ i ++ show a ++ ps'
showProof Unknown = 
  return "Unknown"

instance Show a => JSON (ProofStep a) where
  json (ProofStep step cls) = 
    "{\"name\":\"" ++ step ++ "\",\"clause\":\"" ++ show cls ++ "\"}" 
  
instance JSON a => JSON (Proof a) where
  json Unknown = "\"unknown\""
  json (Proven step inner) = 
    let inner' = intercalate "," $ map json inner
    in "{\"step\":" ++ json step ++ ",\"proof\":[" ++ inner' ++ "]}" 

  
